Computers and accompanying software touch nearly every aspect of our lives. Computers and software extend well beyond the computer workstations used in many vocations. For example, extensive computer systems and supporting software are used in telephone services, both mobile and wired, airline reservation systems, point-of-sale terminals at retail outlets, and at all levels of the health-care industry. As society increasingly relies on computers and software, there is a corresponding rising expectation that the systems will be reliable and not be prone to failure.
Not only are computers and software affecting more daily activities, but the size and complexity of software packages are increasing as well. A software package of previous generations may have been on the order of thousands or tens-of-thousands of lines of code. Today, applications with millions of lines of code are not uncommon. Managing the growth of software while attending to reliability issues challenges even the most talented software developers.
The presence of programming errors, or “bugs,” grows with the size and complexity of software applications. For some applications, bugs may be tolerable. However, for life-critical applications, a bug may result in loss of life. Thus, ensuring that a software package is free of bugs may not only be a desirable part of the software development effort, but a necessary undertaking.
Both manual and automated processes have been used in attempts to verify that a software package is free of bugs. Manual processes include inspection of source code by a developer and colleagues and testing of the software's basic functions while the software is running. Automated processes include software drivers that interact with the software package, as well as software tools that analyze and report deficiencies in the source code.
Manual inspection of source code is costly, time consuming, and limited in effectiveness by the availability of resources, such as time and people. Whether automated or manual, testing may require elaborate set-up procedures, require a great deal of time, and exercise only the main functions of the software package. Thus, some portions of the software package may go untested and bugs go uncovered before the software is deployed for real-life use.
Software tools that analyze source code and report bugs may be very useful in uncovering certain types of bugs. However, one obstacle to finding program errors in a large software package is the availability of the correctness rules that the source code must follow. These rules are often undocumented or specified in an ad hoc manner, which makes assembling the rules for use by a tool difficult. In addition, cost considerations often prohibit manually specifying or discovering all the correctness rules that a large package must obey.